r:. (r - 0) = r 

latex

Definitions	P  Q, P & Q, T, P  Q, P  Q, r - s, True, t  T, x:A. B(x), , S  T
Lemmas	mon ident q, qadd comm q, qinv id q, true wf, squash wf, qadd wf, int inc rationals, rationals wf